p, q:( List), F:({0..||p @ q||}).
weighted-sum(p @ q;F) = (weighted-sum(p;F) + weighted-sum(q;i.F(i+||p||)))   

latex

Definitions	t  T, True, , x:A. B(x), {i..j}, <a, b>, s = t, P  Q, False, A, P & Q, A  B, i  j < k, , {x:A| B(x)} , T, x. t(x), Type, x:AB(x), a  j < b. E(j), i  j , a < b, x:A  B(x), P  Q, P  Q, r + s, n+m, Void, , , s ~ t, {T}, SQType(T), x,y:A//B(x;y), type List, weighted-sum(p;F), as @ bs, l[i], f(a), r * s, x.A(x), ||as||, #$n, n - m
Lemmas	select append back, sum shift q, sum split q, le wf, qadd wf, select append front, qmul wf, select wf, length append, non neg length, qsum wf, squash wf, true wf, int seg wf, length wf1, append wf, rationals wf